Nuprl Lemma : d-eq-Loc_wf
0,22
postcript
pdf
i
,
j
:Id.
i
=
j
latex
Definitions
i
=
j
,
eqof(
d
)
,
x
:
A
.
B
(
x
)
,
IdDeq
,
t
T
,
Id
Lemmas
Id
wf
,
id-deq
wf
,
eqof
wf
origin
i, j:Id. i = j 
i, j:Id. i = j x:A. B(x) T